Require Import AutoSep.
Definition addS := SPEC("n", "m") reserving 0
  PRE[V] [| True |]
  POST[R] [| R = V "n" ^+ V "m" |].
Definition addM := bmodule "add" {{
  bfunction "add"("n", "m") [addS]
    Return "n" + "m"
  end
}}.
Theorem addMOk : moduleOk addM.
Proof.
  vcgen; sep_auto.
Qed.